package no.uio.ifi.cop.prover;

import no.uio.ifi.cop.cl.Axiom;

/**
 * This abstract class works as a default implementation of a rule-node.
 *
 * It gives the default preference, i.e. RuleFinders will typically
 * hold a TreeSet of extended RuleMatcher objects. If more than one
 * RuleMatcher has found a match, the order they are requested is
 * based on the compareTo method, unless it's overridden.
 *
 * @version 1.0
 * @author  bjarneh@ifi.uio.no
 */

public abstract class RuleMatcher implements Comparable<RuleMatcher>{

    int id;
    // the id is needed for the TreeSet i.e., a.compareTo(b) == 0
    // should never be returned unless a == b (same object)

    Axiom axiom;

    public void setId(int ID){ id = ID; }

    public int getId(){ return id; }

    public void setAxiom(Axiom ax){ axiom = ax; }

    public Axiom getAxiom(){ return axiom; }

    public abstract int applications();

    public int compareTo(RuleMatcher other){

        int myType, otherType;
        myType    = axiom.getType();
        otherType = other.getAxiom().getType();

        if( myType < otherType ){
            return -1;
        }else if( myType > otherType ){
            return 1;
        }else{
            if( id < other.getId() ){
                return -1;
            }else if( id > other.getId() ){
                return 1;
            }
        }

        return 0;
    }


    public boolean equals(Object other){
        if(this == other){
            return true;
        }
        if( other instanceof RuleMatcher ){
            RuleMatcher rlm_other = (RuleMatcher) other;
            return id == rlm_other.getId();
        }
        return false;
    }
}
